A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a), x:A.
x  dom(f)  f  g(x) = f(x)  B(x) 

latex

Definitions	2of(t), f(x), Top, a:A fp B(a), EqDecider(T), f  g, f(x)?z, Unit, P  Q, P & Q, x  dom(f), x(s), x. t(x), , Prop, b, t  T, b, x:A. B(x), A, P  Q, False
Lemmas	not wf, bnot wf, assert wf, fpf-ap wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, fpf wf, fpf-trivial-subtype-top